E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)).
SWellFounded(pred!(e;e'))
 (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 (e,e':E. (loc(e) = loc(e')  Id)  (pred?(e) = pred?(e'))  (e = e'))
 (e,e':E.
 (loc(e) = loc(e')  Id)
  e < e'
  (e rel_plus(E; (x,y. ((first(y))) c (x = pred(y)  E))) e')) 

latex

Definitions	trans(T; x,y.E(x;y)), rel_implies(T; R1; R2), x. t(x), P  Q, P  Q, rcv?(e), sender(e), A c B, guard(T), x f y, rel_plus(T; R), e < e', b, first(e), prop{i:l}, pred(e), loc(e), SWellFounded(R(x;y)), x,y. t(x;y), pred!(e;e'), Unit, Id, IdLnk, t  T, x:A. B(x), A, False, P  Q, wellfounded{i:l}(A; x,y.R(x;y))
Lemmas	pred-total, IdLnk wf, Id wf, unit wf, pred! wf, strongwellfounded wf, loc wf, pred wf, first wf, assert wf, not wf, cless wf, wellfounded functionality wrt implies, strongwf-implies, sender wf, rcv? wf, rel plus strongwellfounded, rel plus monotone, rel plus trans